package minsat;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;

/**
 * Represents a set of vertices and their connections to each other. Used by MinSatz to calculate
 * max-cliques in order to estimate an upper bound of unsatisfiable soft clauses.
 */
public class Graph
{
  private Vertex[] vertices;
  private int vertexCount;

  public Graph(int numVertices)
  {
    vertices = new Vertex[numVertices];
    vertexCount = 0;
  }

  public void addVertex(int index, double weight)
  {
    vertices[index] = new Vertex(index, weight);
    vertexCount++;
  }

  public void addEdge(int source, int target)
  {
    vertices[source].addEdge(target);
    vertices[target].addEdge(source);
  }

  public boolean hasEdge(int source, int target)
  {
    return vertices[source].hasEdge(target);
  }

  public void removeVertex(int index)
  {
    for (Integer v : vertices[index].getNeighbors())
      vertices[v].removeEdge(index);
    vertices[index] = null;
    vertexCount--;
  }

  public int getSize()
  {
    return vertexCount;
  }

  public List<Vertex> sortedByDegree()
  {
    ArrayList<Vertex> toSort = new ArrayList<Vertex>(vertexCount);
    for (int i = 0; i < vertices.length; i++)
      if (vertices[i] != null) {
        toSort.add(vertices[i]);
      }
    Collections.sort(toSort);

    return toSort;
  }

  /**
   * Decrements the weights of each vertex in a clique by the clique's weight and then removes the
   * minimum vertex
   * 
   * @return Weight of the clique
   */
  public double decrementWeightAndRemove(List<Vertex> clique)
  {
    // first find the clique's weight
    double weight = clique.get(0).getWeight();
    for (Vertex v : clique) {
      if (v.getWeight() < weight) weight = v.getWeight();
    }

    // now decrement weights and remove any that hit 0
    for (Vertex v : clique) {
      if (v.getWeight() - weight == 0)
        removeVertex(v.getIndex());
      else
        vertices[v.getIndex()].decreaseWeight(weight);
    }
    return weight;
  }

  /**
   * Gets the max clique for the first vertex in the sorted list of vertices sorted by increasing
   * degree
   */
  public List<Vertex> maxClique(List<Vertex> sorted)
  {
    boolean valid;
    Vertex v = sorted.get(0);
    ArrayList<Vertex> bestSoFar = new ArrayList<Vertex>();

    // if this is a single vertex or an isolated vertex, return it
    if (sorted.size() == 1 || v.getNeighbors().isEmpty()) {
      bestSoFar.add(v);
      return bestSoFar;
    }

    // the biggest clique possible contains all neighbors and myself
    int bestPossible = v.getDegree() + 1;

    // for each of my neighbors (in order), build the biggest clique containing that neighbor
    ArrayList<Vertex> neighborBest;
    Vertex neighbor;

    // consider neighbors in decreasing order of degree
    for (int i = sorted.size() - 1; i >= 0; i--) {
      // only consider this vertex if it is a neighbor of v
      if (v.getNeighbors().contains(sorted.get(i).getIndex())) {
        neighbor = sorted.get(i);

        if (neighbor.getDegree() + 1 < bestSoFar.size()) {
          // this neighbor can't possibly be part of a larger clique
          continue;
        }

        neighborBest = new ArrayList<Vertex>();
        neighborBest.add(v); // v must be in the clique

        // check each of my neighbor's links
        for (Integer nn : neighbor.getNeighbors()) {
          if (nn.equals(v.getIndex()))
            continue; // already added
          else {
            valid = true;
            for (Vertex currentMember : neighborBest) {
              // assert that this vertex is connected to everything already in the clique
              if (!currentMember.getNeighbors().contains(nn)) {
                valid = false;
                break; // fail fast
              }
            }
            if (valid) neighborBest.add(vertices[nn]); // add a shared link
          }
        }

        neighborBest.add(neighbor); // add the neighbor

        // if this is better than the best we have so far, update the best we have so far
        if (neighborBest.size() > bestSoFar.size()) bestSoFar = neighborBest;

        // update best possible size without the current neighbor
        bestPossible--;

        if (bestSoFar.size() >= bestPossible) {
          return bestSoFar;
        }
      }
    }

    return bestSoFar;
  }

  /**
   * Compute a reasonable upper bound of satisfiable weights based on the current graph.
   * 
   * @return Upper bound of weights before applying unit propagation
   */
  public double getUpperBound()
  {
    double sum = 0;

    List<Vertex> sorted = sortedByDegree();

    // continue until the empty graph is derived
    while (!sorted.isEmpty()) {
      sum += decrementWeightAndRemove(maxClique(sorted));
      sorted = sortedByDegree();
    }
    return sum;
  }

  public String toString()
  {
    String result = "Graph:\n";
    for (Vertex v : vertices)
      result += v + "\n";
    return result;
  }
}
